a,b:Id. decidable((a = b)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, prop{i:l}, t  T, x. t(x), P  Q, P  Q, x(s)
Lemmas	all functionality wrt iff, Id wf, decidable wf, assert wf, eq id wf, decidable functionality, assert-eq-id, decidable assert